/LMAR=0/XLINE=3/FONT#0=BAXL30[FNT,CLT]/FONT#1=BAXM30/FONT#2=BAXB30[FNT,CLT]/FONT#5=GACS25/FONT#3=SUB/FONT#4=SUP/FONT#7=SYMB30[FNT,CLT]

␈↓ ↓H␈↓␈↓ ∧+COMPUTER SCIENCE DEPARTMENT
␈↓ ↓H␈↓␈↓ ¬πSTANFORD UNIVERSITY
␈↓ ↓H␈↓CS206  ␈↓ βiRECURSIVE PROGRAMMING AND PROVING ␈↓ 
0FALL 1979
␈↓ ↓H␈↓␈↓ ¬DPROBLEM SET  3
␈↓ ↓H␈↓␈↓ ¬kDue  Nov. 12?

␈↓ ↓H␈↓1.  Consider the program ␈↓↓flatagain[x]␈↓ defined as follows:

␈↓ ↓H␈↓␈↓↓flatagain x ← flata[<x>,␈↓¬NIL␈↓↓]␈↓
␈↓ ↓H␈↓␈↓↓flata[u,v] ← ␈↓αif␈↓↓ ␈↓αn|␈↓↓u ␈↓αthen␈↓↓ v ␈↓αelse␈↓↓ ␈↓αif␈↓↓ ␈↓αat|␈↓↓␈↓αa|␈↓↓u ␈↓αthen␈↓↓ flata[␈↓αd|␈↓↓u,␈↓αa|␈↓↓u . v] ␈↓αelse␈↓↓ flata[␈↓αda|␈↓↓u . [␈↓αaa|␈↓↓u . ␈↓αd|␈↓↓u],v]␈↓

␈↓ ↓H␈↓        Prove␈α
that␈α
␈↓↓flatagain␈↓␈α
is␈α
total␈αon␈α
S-expressions␈α
(␈↓↓∀x:SEXP flatagain x␈↓)␈α
and␈α
that␈α
it␈αcomputes
␈↓ ↓H␈↓␈↓ ↓xthe␈α∂same␈α∂function␈α∂as␈α∂␈↓↓fringe␈↓␈α⊂ (␈↓↓∀x:flatagain x=fringe x␈↓).␈α∂ The␈α∂actual␈α∂solution␈α∂to␈α⊂this␈α∂problem
␈↓ ↓H␈↓␈↓ ↓xshould␈α
be␈αquite␈α
short,␈αbut␈α
it␈αwill␈α
require␈αinventing␈α
a␈αsuitable␈α
intermediate␈αtheorem␈α
to␈αprove,
␈↓ ↓H␈↓␈↓ ↓xand figuring out a rank function to use for the induction.

␈↓ ↓H␈↓2.␈α∀ This␈α∪problem␈α∀is␈α∪designed␈α∀to␈α∪lead␈α∀you␈α∪through␈α∀the␈α∪development␈α∀of␈α∪a␈α∀theory␈α∀about␈α∪an
␈↓ ↓H␈↓␈↓ ↓xinductively␈α∞defined␈α∞domain,␈α∞␈↓↓BOOL,␈↓␈α∞of␈α∞boolean␈α∞expressions.␈α∞ We␈α∞then␈α∞represent␈α∞elements␈α
of
␈↓ ↓H␈↓␈↓ ↓xthis␈αdomain␈αas␈αS-expressions,␈αand␈αprove␈αthe␈αrepresentation␈αcorrect.␈α We␈αcan␈αthen␈αwrite␈αLISP
␈↓ ↓H␈↓␈↓ ↓xprograms␈α∞to␈α∞compute␈α∂functions␈α∞or␈α∞predicates␈α∞on␈α∂the␈α∞␈↓↓BOOL␈↓␈α∞and␈α∞use␈α∂the␈α∞theory␈α∞of␈α∂␈↓↓BOOL␈↓␈α∞to
␈↓ ↓H␈↓␈↓ ↓xreason about these programs.

␈↓ ↓H␈↓The domain of boolean expressions, ␈↓↓BOOL,␈↓ is defined inductively as follows.

␈↓ ↓H␈↓          (i) ␈↓↓BT␈↓ boolean expression satisfying ␈↓↓BOOLT␈↓
␈↓ ↓H␈↓         (ii) ␈↓↓BF␈↓ boolean expression satisfying ␈↓↓BOOLF␈↓
␈↓ ↓H␈↓        (iii) A boolean variable is a boolean expression satisfying ␈↓↓BOOLV␈↓
␈↓ ↓H␈↓         (iv) If ␈↓↓be␈↓ is boolean expression then the negation
␈↓ ↓H␈↓                ␈↓↓mknot[be]␈↓ is a boolean expression satisfying ␈↓↓BOOLN␈↓
␈↓ ↓H␈↓          (v) If ␈↓↓be1␈↓ and ␈↓↓be2␈↓ are boolean expressions then the conjuction
␈↓ ↓H␈↓                ␈↓↓mkand[be1,be2]␈↓ is a boolean expression satisfying ␈↓↓BOOLA.␈↓
␈↓ ↓H␈↓         (vi) The only boolean expressions are those that are required by (i)-(v).
␈↓ ↓H␈↓              Each boolean expression is uniquely determined by its construction via successive
␈↓ ↓H␈↓                applications of (i)-(v)

␈↓ ↓H␈↓        We␈αhave␈αthe␈αfunction␈α␈↓↓pn␈↓␈αdefined␈αon␈αthe␈αsubdomain␈α␈↓↓BOOLN␈↓␈αwhich␈αreturns␈αthe␈αcomponent
␈↓ ↓H␈↓␈↓ ↓xexpression,␈α
the␈α
functions␈α∞␈↓↓pa1,␈↓␈α
␈↓↓pa2␈↓␈α
defined␈α∞on␈α
the␈α
subdomain␈α∞␈↓↓BOOLA␈↓␈α
which␈α
select␈α∞the␈α
first
␈↓ ↓H␈↓␈↓ ↓xand second components, respectively.

␈↓ ↓H␈↓2.1.␈α
 Give␈α
domain␈αspecifications,␈α
domain␈α
range␈α
mappings␈αand␈α
axioms␈α
characterizing␈α
the␈αdomain
␈↓ ↓H␈↓␈↓ ↓xof boolean expressions.   In particular you should

␈↓ ↓H␈↓(i)␈α⊃You␈α⊃should␈α⊃express␈α⊃the␈α∩appropriate␈α⊃domain/range␈α⊃specifications␈α⊃for␈α⊃the␈α∩functions␈α⊃␈↓↓mknot,␈↓
␈↓ ↓H␈↓␈↓ ↓x␈↓↓mkand,␈↓ ␈↓↓mkor,␈↓ ␈↓↓pn,␈↓ ␈↓↓pa1,␈↓ ␈↓↓pa2,␈↓ ␈↓↓po1␈↓ and ␈↓↓po2.␈↓
␈↓ ↓H␈↓(ii)␈α The␈αdomain␈αrelations␈αshould␈αexpress␈αthe␈αfact␈αthat␈αeach␈αboolean␈αexpression␈αbelongs␈αto␈αexactly
␈↓ ↓H␈↓␈↓ ↓xone of the subdomains ␈↓↓BOOLT,␈↓ ␈↓↓BOOLF,␈↓ ␈↓↓BOOLV,␈↓ ␈↓↓BOOLN␈↓ or ␈↓↓BOOLA.␈↓
␈↓ ↓H␈↓(iii)␈α Provide␈αfor␈αvariables␈α␈↓↓be,␈↓␈α␈↓↓be1,␈↓␈α...␈αranging␈αover␈αboolean␈αexpressions,␈α␈↓↓bv,␈↓␈α␈↓↓bv1,␈↓␈α...␈αranging␈αover
␈↓ ↓H␈↓␈↓ ↓xboolean␈α∃variables,␈α∃␈↓↓bn,␈↓␈α∃␈↓↓bn1,␈↓␈α∃...␈α∃ranging␈α∃over␈α∃negations,␈α∃and␈α∃␈↓↓ba,␈↓␈α∃␈↓↓ba1,␈↓␈α∃...␈α∃ranging␈α∃over
␈↓ ↓H␈↓␈↓ ↓xconjunctions.
␈↓ ↓H␈↓(iv)␈α The␈αaxioms␈αshould␈αexpress␈αthe␈αalgebraic␈αrelations␈αfor␈αthe␈αselector␈αand␈α
constructor␈αfunctions
␈↓ ↓H␈↓␈↓ ↓xfor␈α∪negations␈α∪and␈α∩conjuctions.␈α∪ Also␈α∪give␈α∩the␈α∪axiom␈α∪schema␈α∩for␈α∪structural␈α∪induction␈α∩on
␈↓ ↓H␈↓␈↓ ↓xboolean expressions.
␈↓ ↓H␈↓2␈↓ H


␈↓ ↓H␈↓2.2.␈α⊃ Decide␈α⊃on␈α⊃a␈α⊃representation␈α⊃of␈α⊃boolean␈α⊃expressions␈α⊃as␈α⊃S-expressions␈α⊃and␈α⊃write␈α⊂programs
␈↓ ↓H␈↓␈↓ ↓ximplementing␈αthis␈αrepresentation.␈α You␈α
will␈αneed␈αa␈αprogram␈α
to␈αdecide␈αwhether␈αan␈αarbitrary␈α
S-
␈↓ ↓H␈↓␈↓ ↓xexpression␈αrepresents␈αa␈αboolean␈α
expression.␈α You␈αwill␈αalso␈α
need␈αprograms␈αfor␈αeach␈α
subdomain,
␈↓ ↓H␈↓␈↓ ↓xto␈α↔decide␈α↔whether␈α↔a␈α↔boolean␈α↔expression␈α↔(e.g.␈α↔an␈α↔S-expression␈α↔representing␈α↔a␈α↔boolean
␈↓ ↓H␈↓␈↓ ↓xexpression)␈α
is␈αa␈α
member␈αof␈α
that␈αsubdomain,␈α
and␈αprograms␈α
implementing␈αthe␈α
constructor␈αand
␈↓ ↓H␈↓␈↓ ↓xselector functions.

␈↓ ↓H␈↓2.3.␈α Prove␈αthat␈αyour␈αrepresentation␈αis␈αcorrect.␈α E.g.␈αgive␈αthe␈αaxioms␈αcharacterizing␈αyour␈αprograms
␈↓ ↓H␈↓␈↓ ↓xas␈α⊃functions␈α⊃on␈α⊃S-expressions␈α⊃and␈α⊃show␈α⊃that␈α⊃the␈α⊃computed␈α⊃domain␈α⊃predicates␈α∩satisfy␈α⊃the
␈↓ ↓H␈↓␈↓ ↓xdomain␈α∪relations␈α∪and␈α∪that␈α∪the␈α∩selector␈α∪and␈α∪constructor␈α∪functions␈α∪obey␈α∪the␈α∩domain/range
␈↓ ↓H␈↓␈↓ ↓xspecifications and satisfy the algebraic axioms.

␈↓ ↓H␈↓2.4.␈α⊂Write␈α⊂an␈α⊂interpreter␈α⊂␈↓↓beval[be,alist]␈↓␈α⊂which␈α⊂computes␈α⊂the␈α⊂value␈α⊂(a␈α⊂boolean␈α⊂constant)␈α⊂of␈α⊂the
␈↓ ↓H␈↓␈↓ ↓xexpression␈α␈↓↓be␈↓␈α
using␈αto␈α
the␈αassignment␈αof␈α
values␈αto␈α
variables␈αgiven␈αby␈α
␈↓↓alist␈↓␈αand␈α
the␈αfollowing
␈↓ ↓H␈↓␈↓ ↓xrules:

␈↓ ↓H␈↓␈↓ αH␈↓↓BT → BT␈↓
␈↓ ↓H␈↓␈↓ αH␈↓↓BF → BF␈↓
␈↓ ↓H␈↓␈↓ αH␈↓↓mknot BT → BF␈↓
␈↓ ↓H␈↓␈↓ αH␈↓↓mknot BF → BT␈↓
␈↓ ↓H␈↓␈↓ αH␈↓↓mkand[BT,BT] → BT␈↓
␈↓ ↓H␈↓␈↓ αH␈↓↓mkand[BT,BF] → BF␈↓
␈↓ ↓H␈↓␈↓ αH␈↓↓mkand[BF,BT] → BF␈↓
␈↓ ↓H␈↓␈↓ αH␈↓↓mkand[BF,BF] → BF␈↓

␈↓ ↓H␈↓2.5.  Notice that according to the above rules we have the following property:

␈↓ ↓H␈↓␈↓ αH␈↓↓∀be alist.beval[mknot[BT],alist]=BF]␈↓
␈↓ ↓H␈↓␈↓ αH␈↓↓∀be alist.beval[mknot[BF],alist]=BT]␈↓
␈↓ ↓H␈↓␈↓ αH␈↓↓∀be alist.beval[mkand[BT,be],alist]=beval[be,alist]]␈↓
␈↓ ↓H␈↓␈↓ αH␈↓↓∀be alist.beval[mkand[be,BT],alist]=beval[be,alist]]␈↓
␈↓ ↓H␈↓␈↓ αH␈↓↓∀be alist.beval[mkand[BF,be],alist]=BF␈↓
␈↓ ↓H␈↓␈↓ αH␈↓↓∀be alist.beval[mkand[be,BF],alist]=BF␈↓

␈↓ ↓H␈↓Write␈αa␈αprogram␈α
␈↓↓bsimplify[be]␈↓␈αwhich␈αreduces␈α␈↓↓be␈↓␈α
to␈αa␈αconstant␈αis␈α
possible␈αand␈αother␈α
wise␈αremoves
␈↓ ↓H␈↓␈↓ ↓xall␈α∂occurrences␈α∂of␈α∂constants␈α∂in␈α∂the␈α∞expression␈α∂by␈α∂applying␈α∂the␈α∂above␈α∂facts␈α∂as␈α∞simplification
␈↓ ↓H␈↓␈↓ ↓xrules.

␈↓ ↓H␈↓2.6.  Prove that your program is sound with respect to the interpreter.  That is prove

␈↓ ↓H␈↓␈↓ β≤␈↓↓∀be alist.[binds[be,alist]⊃beval[bsimplify[be],alist]=beval[be,alist]]]␈↓ 

␈↓ ↓H␈↓2.7.  Prove that your program returns a maximally simplified expression.  Namely, prove that

␈↓ ↓H␈↓        ␈↓↓∀be: bsimplest[bsimplify[be]]␈↓
␈↓ ↓H␈↓where
␈↓ ↓H␈↓        ␈↓↓∀be: bsimplest[be]≡BOOLT be ∨ BOOLF be ∨ bsimpv[be]␈↓
␈↓ ↓H␈↓        ␈↓↓∀be:[[bsimplv[be]≡BOOLV be ∨ ␈↓
␈↓ ↓H␈↓        ␈↓↓               [BOOLN be ∧ bsimpv[pn be]] ∨ ␈↓
␈↓ ↓H␈↓        ␈↓↓               [BOOLA be ∧ bsimpv[pa1 be] ∧ bsimpv[pa1 be]] ]␈↓